1. Field of the Invention
The present invention relates to a logic circuit verifying system and method for checking whether or not two combinational logic circuits having no internal states are equivalent with each other.
2. Description of the Related Art
When a logic circuit is designed, the configuration of the circuit is normally amended without changing the function of the originally designed circuit to satisfactorily meet the restrictive conditions relating to the number of gates, delay time, etc. Such a circuit amendment can be automatically made by a computer program, but is normally performed manually by its skilled designer. At this time, it is necessary to verify the functional equivalence of the circuits before and after the amendment to prevent the functions of the circuit from being changed by a mis-amendment. Thus, it is very important in circuit designing to verify the equivalence of logic circuits.
One equivalence verifying method is followed by applying the same input pattern to two circuits, performing a logical simulation, and checking whether or not the same output value is obtained from the two circuits. However, in this method, the equivalence is not verified unless all input patterns are checked. Assuming that the number of inputs external to the circuit is n, the number of patterns required for verification is 2.sup.n. If the value n refers to several tens, it is almost impossible to simulate all patterns.
Another equivalence verifying method is followed by representing a logical function of an output external to the circuit as data structure, referred to as a dichotomizing decision graph, and checking whether or not the dichotomizing graphs of the outputs external to the two circuits are similar to each other. However, the dichotomizing decision graph may not be prepared, using this method, by using the explosion of the nodal points on the graph, depending on the scale and properties of the circuit.
On the other hand, Kunz and others have suggested a method for verifying the equivalence through an indirect implication referred to as a recursive learning (W. Kunz and D. K. Pradhan, "Recursive learning: A new implication technique for efficient solutions to CAD problems--test, verification, and optimization.", in IEEE Trans. on Computer-aided Design of Integrated Circuits and systems, Vol, 13, No. 9, pages 1143-1157, September, 1994, Hannibal). Reddy and others have suggested a combination of the recursive learning and the dichotomizing decision graph (S. M. Reddy, W. Kunz and D. K. Pradhan, "Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment", in Proc. 32nd Design Automation conf., pp. 414-419, June 1995).
According to Reddy and others, a set of equivalent internal signal lines in two circuits is obtained using the recursive learning, and an equivalent internal signal line closest to the external output is defined as a pseudo-input. Using the pseudo-input, the logical functions of the external outputs are generated and compared between the two corresponding external outputs. In this method, the explosion of the number of nodal points on the dichotomizing decision graph can be suppressed by generating the logical functions with the internal signal lines of the circuits applied as pseudo-inputs. When the two compared logical functions are equal to each other, the equivalence of the circuits is verified, but the equivalence is not necessarily verified if the logical functions are not equal to each other.
FIG. 1A shows an example of equivalent circuits having different structures. In FIG. 1A, the left circuit comprises a NAND gate 1, AND gates 2 and 3, and OR gate 4, and generates an output signal x1 from input signals A, B, and C. The right circuit comprises a NAND gate 5, AND gates 6 and 7, and XOR (exclusive or) gate 8, and generates an output signal x2 from input signals A, B, and C. These two circuits are different in element of the output stages, but are equivalent in entire circuit. When the equivalence of circuits is verified by the method of Reddy and others, the input signals s1 and t1 of the OR gate 4 and the input signals s2 and t2 of the XOR gate 8 are used as pseudo-inputs of a logical function. However, the logical function of the external output x1 generated by inputting s1 and t1 is quite different from the logical function of the external output x2 generated by inputting s2 and t2.
In this case, it should be furthermore checked whether or not the set of the internal signal lines which are used as the pseudo-input can be values that generate different external outputs. Reddy and others temporarily assign 0 or 1 to the internal signal lines, and determines that the circuits are not equivalent if all assignments are performed without inconsistency and the external outputs are different from each other. It is determined that the circuits are equivalent if assigning values to make different external outputs generates inconsistency.
Jain and others also suggests an equivalence verifying method similar to that suggested by Reddy and others (J. Jain, R. Mukherjerr and M. Fujita, "Advanced Verification Techniques Based on Learning", in Proc. 32nd Design automation conf., pp. 420-426, June 1995). The method suggested by Jain and others also generates logical functions of two external outputs with the equivalent internal signal lines closest to the external outputs used as pseudo-inputs, and determines that the circuits are equivalent if the generated functions are equal to each other. If they are not equal to each other, it is checked whether or not a set of internal signal lines applied as a pseudo-input can refer to values to generate different external outputs. In the verification, a set of signal lines closer to the external inputs than the internal signal lines used as pseudo-inputs is selected and defined as a new pseudo input. Using the original pseudo-input signal lines as a pseudo-output, the logical function of the output is generated, and it is checked whether or not an input which causes different external outputs exists.
According to the methods of Reddy and Jain, the relationship between internal signal lines is first obtained by a relatively high-speed, but not definite determining method, and then an equivalence verification is performed between the internal signal lines closer to output terminals or on external outputs according to the obtained relationship. However, as shown in FIG. 1B, when two circuits, which are equivalent in function of external output but different in configuration closer to external inputs are verified, those methods are not necessarily effective.
In FIG. 1B, one logical circuit comprises combinational circuits 9 and 10, and the other logical circuit comprises combinational circuits 11 and 12. The combinational circuits 9 and 11 are equivalent in function, but different in structure. The combinational circuits 10 and 12 have the same structure. With these circuits, since the combinational circuits 9 and 11, which are close to an external input, are different from each other in the first high-speed determining method, there may be no equivalent internal signal lines between two logic circuits. In this case, it may require a long time to determine the equivalence of external outputs, or a process may not be performed within a practical time.
For example, if internal signal lines i1, i2, . . . , iN are equivalent to internal signal lines j1, j2, . . . , jN in FIG. 1B, it is determined that all signal lines contained in the combinational circuits 10 and 12 are equivalent because the partial circuits at the output terminals of these signal lines have the same structure. However, in the recursive learning used in the method suggested by Reddy, etc., 2.sup.m cases can be assumed based on the number m of signal lines to which values are assigned, and a practical process cannot be performed if m refers to several tens. Therefore, if a larger-scale circuit is to be verified, the number of cases should be limited. As a result, there is the possibility of failing to recognize that the internal signal lines i1, i2, . . . , iN are equivalent to the internal signal lines j1, j2, . . . , jN. At this time, the internal signal lines in the combinational circuits 9 and 11 are to be checked. However, since these circuits are different in structure, it is hard to detect equivalent internal signal lines.
Furthermore, according to the functional learning suggested by Jain and others, a new set of internal signal lines should be selected if a comparison is made after generating a logical function using a set of internal signal lines to be first verified as a pseudo-input. However, it is not practically indicated which internal signal line is traced back to generate the logical function. If an internal signal line is selected through a number of attempts, there is the possibility of failing to recognize that the internal signal lines i1, i2, . . . , iN are equivalent to the internal signal lines j1, j2, . . . , jN, thereby causing the problem similar to that of the recursive learning.
Thus, the conventional equivalence verifying methods cannot completely verify the equivalence of the internal signal lines, and cannot be used as methods for practical use.